Theorem 3com23 1271

Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com23	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Proof of Theorem 3com23

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1264	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 86	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	3imp 1256	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3coml  1272  syld3an2  1373  3anidm13  1384  eqreu  3398  f1ofveu  6645  curry2f  7273  dfsmo2  7444  nneob  7732  f1oeng  7974  suppr  8377  infdif  9031  axdclem2  9342  gchen1  9447  grumap  9630  grudomon  9639  mul32  10203  add32  10254  subsub23  10286  subadd23  10293  addsub12  10294  subsub  10311  subsub3  10313  sub32  10315  suble  10506  lesub  10507  ltsub23  10508  ltsub13  10509  ltleadd  10511  div32  10705  div13  10706  div12  10707  divdiv32  10733  cju  11016  infssuzle  11771  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  fzen  12358  modcyc  12705  expgt0  12893  expge0  12896  expge1  12897  2cshwcom  13562  shftval2  13815  abs3dif  14071  divalgb  15127  submrc  16288  mrieqv2d  16299  pltnlt  16968  pltn2lp  16969  tosso  17036  latnle  17085  latabs1  17087  lubel  17122  ipopos  17160  grpinvcnv  17483  mulgneg2  17575  oppgmnd  17784  oddvdsnn0  17963  oddvds  17966  odmulg  17973  odcl2  17982  lsmcomx  18259  srgrmhm  18536  ringcom  18579  mulgass2  18601  opprring  18631  irredrmul  18707  irredlmul  18708  isdrngrd  18773  islmodd  18869  lmodcom  18909  rmodislmod  18931  opprdomn  19301  zntoslem  19905  ipcl  19978  maducoevalmin1  20458  rintopn  20714  opnnei  20924  restin  20970  cnpnei  21068  cnprest  21093  ordthaus  21188  kgen2ss  21358  hausflim  21785  fclsfnflim  21831  cnpfcf  21845  opnsubg  21911  cuspcvg  22105  psmetsym  22115  xmetsym  22152  ngpdsr  22409  ngpds2r  22411  ngpds3r  22413  clmmulg  22901  cphipval2  23040  iscau2  23075  dgr1term  24016  cxpeq0  24424  cxpge0  24429  relogbzcl  24512  grpoidinvlem2  27359  grpoinvdiv  27391  nvpncan  27509  nvabs  27527  ipval2lem2  27559  dipcj  27569  diporthcom  27571  dipdi  27698  dipassr  27701  dipsubdi  27704  hlipcj  27767  hvadd32  27891  hvsub32  27902  his5  27943  hoadd32  28642  hosubsub  28676  unopf1o  28775  adj2  28793  adjvalval  28796  adjlnop  28945  leopmul2i  28994  cvntr  29151  mdsymlem5  29266  sumdmdii  29274  supxrnemnf  29534  odutos  29663  tlt2  29664  tosglblem  29669  archiabl  29752  unitdivcld  29947  bnj605  30977  bnj607  30986  gcd32  31637  cgrrflx  32094  cgrcom  32097  cgrcomr  32104  btwntriv1  32123  cgr3com  32160  colineartriv2  32175  segleantisym  32222  seglelin  32223  btwnoutside  32232  clsint2  32324  dissneqlem  33187  ftc1anclem5  33489  heibor1  33609  rngoidl  33823  ispridlc  33869  opltcon3b  34491  cmtcomlemN  34535  cmtcomN  34536  cmt3N  34538  cmtbr3N  34541  cvrval2  34561  cvrnbtwn4  34566  leatb  34579  atlrelat1  34608  hlatlej2  34662  hlateq  34685  hlrelat5N  34687  snatpsubN  35036  pmap11  35048  paddcom  35099  sspadd2  35102  paddss12  35105  cdleme51finvN  35844  cdleme51finvtrN  35846  cdlemeiota  35873  cdlemg2jlemOLDN  35881  cdlemg2klem  35883  cdlemg4b1  35897  cdlemg4b2  35898  trljco2  36029  tgrpabl  36039  tendoplcom  36070  cdleml6  36269  erngdvlem3-rN  36286  dia11N  36337  dib11N  36449  dih11  36554  nerabdioph  37373  monotoddzzfi  37507  fzneg  37549  jm2.19lem2  37557  nzss  38516  sineq0ALT  39173  lincvalsng  42205  reccot  42499