Theorem 3expd 1213

Description: Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.)

Hypothesis

Ref	Expression
3expd.1

Assertion

Ref	Expression
3expd

Proof of Theorem 3expd

Step	Hyp	Ref	Expression
1		3expd.1	. . . 4
2	1	com12 31	. . 3
3	2	3exp 1195	. 2
4	3	com4r 86	1

Syntax hints:  ->wi 4  /\w3a 973

This theorem is referenced by:  3exp2  1214  exp516  1216  smogt  7057  axdc3lem4  8854  axcclem  8858  caubnd  13191  catidd  15077  mulgnnass  16170  bwthOLD  19911  mclsind  28930  fscgr  29730  3impexp  33220  3impexpbicom  33221  cvrat4  35167  3dim1  35191  3dim2  35192  llnle  35242  lplnle  35264  llncvrlpln2  35281  lplncvrlvol2  35339  pmaple  35485  paddasslem14  35557  paddasslem15  35558  osumcllem11N  35690  cdlemeg46gfre  36258  cdlemk33N  36635  dia2dimlem6  36796  lclkrlem2y  37258  cotr2g  37786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975