Theorem 3expia 1121

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 456	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ad5ant125  1368  mp3an3  1452  3gencl  3509  vtocl3gaf  3565  vtocl3ga  3567  moi  3706  disji  5109  disjord  5113  3optocl  5756  sossfld  6180  f1oresrab  7122  f1cdmsn  7280  soisores  7325  isomin  7335  isofrlem  7338  ovmpos  7560  ov2gf  7561  ndmovord  7602  nnsuc  7884  poxp  8132  frpoins3xp3g  8145  brtpos  8239  dfsmo2  8366  smoiun  8380  smoord  8384  smogt  8386  omeulem1  8599  omeu  8602  oewordi  8608  uniinqs  8816  mapvalg  8855  pmvalg  8856  elmapg  8858  xpdom3  9089  mapdom3  9168  sdomdomtrfi  9220  domsdomtrfi  9221  php  9226  php3  9228  nndomog  9232  php3OLD  9238  onomeneq  9242  sucdom  9248  unxpdomlem3  9265  isinf  9273  isinfOLD  9274  f1finf1o  9282  isfinite2  9311  prfi  9340  ordiso  9535  cnfcom3clem  9724  r111  9794  tskwe  9969  pr2ne  10023  pr2neOLD  10024  infxpenlem  10032  dfac8alem  10048  infdif  10227  infdif2  10228  cff1  10277  coflim  10280  cfslbn  10286  cfslb2n  10287  cofsmo  10288  cfsmolem  10289  cfcoflem  10291  fin23lem27  10347  isf32lem9  10380  isf34lem6  10399  axcc2lem  10455  domtriomlem  10461  axdc4lem  10474  zorn2lem2  10516  axdclem2  10539  konigthlem  10587  gchen1  10644  gchen2  10645  gchpwdom  10689  gchaleph  10690  winainflem  10712  tskcard  10800  gruiun  10818  gruen  10831  intgru  10833  grudomon  10836  grur1a  10838  grutsk1  10840  nqereu  10948  nqereq  10954  ltsonq  10988  prlem934  11052  reclem3pr  11068  1re  11240  axsup  11315  addlid  11423  recex  11874  lemul1a  12100  lt2msq  12132  fimaxre2  12192  zdiv  12668  zextlt  12672  prime  12679  uzind2  12691  fzind  12696  lbzbi  12957  qbtwnxr  13221  qextltlem  13223  xralrple  13226  xltneg  13238  xlt2add  13281  supxrgtmnf  13350  ixxub  13388  ixxlb  13389  ioo0  13392  ico0  13413  ioc0  13414  icc0  13415  iocssre  13449  icossre  13450  iccssre  13451  fzen  13563  expclzlem  14106  expaddz  14129  expmulz  14131  hashgadd  14400  hashunsngx  14416  hashgt23el  14447  elovmpowrd  14581  pfxnd0  14711  ccatopth2  14740  pfxccatin12  14756  cshf1  14833  shftuz  15093  cau3lem  15378  caubnd  15382  climuni  15573  lo1resb  15585  o1resb  15587  o1of2  15634  o1add  15635  o1mul  15636  o1sub  15637  ntrivcvgmul  15923  eflt  16140  moddvds  16288  dvdscmulr  16309  dvdsmulcr  16310  dvdsle  16334  divalglem8  16424  divalgb  16428  ndvdssub  16433  bitsfzo  16459  gcdcllem1  16523  gcdcllem3  16525  dvdsgcd  16568  nn0rppwr  16585  nn0expgcd  16588  lcmgcdlem  16630  lcmfeq0b  16654  qredeu  16682  isprm3  16707  prmdvdsexpr  16741  prmexpb  16743  eulerthlem2  16806  fermltl  16808  coprimeprodsq  16833  pythagtrip  16859  pcprendvds  16865  pcpremul  16868  pcdvdsb  16894  pc2dvds  16904  4sqlem12  16981  4sqlem18  16987  vdwlem10  17015  cshwshashlem3  17122  xpsrnbas  17590  ismred  17619  mrieqv2d  17656  iscatd  17690  isfuncd  17883  fthestrcsetc  18167  fthsetcestrc  18182  poslubd  18428  dirtr  18617  mulgaddcom  19086  ghmrn  19217  pmtrprfv3  19440  mndodcongi  19529  oddvdsnn0  19530  oddvds  19533  odcl2  19551  odhash3  19562  gexdvds  19570  pgpfi  19591  lsmss1b  19652  lsmss2b  19654  efgsrel  19720  efgred  19734  cntzcmn  19826  cyggenod  19870  lt6abl  19881  gsumcom2  19961  pgpfac1lem2  20063  pgpfac1lem3  20065  dvdsunit  20344  unitmulclb  20346  irredrmul  20392  isabvd  20777  lmodvsdi  20847  lss0cl  20909  islbs3  21121  lbsextlem2  21125  xrsdsreclblem  21385  psrbaglefi  21891  mvrf1  21951  coe1fzgsumd  22247  gsummoncoe1  22251  evl1gsumd  22300  scmataddcl  22459  scmatsubcl  22460  mdetunilem9  22563  mdetuni0  22564  mdetmul  22566  m2cpmrngiso  22701  pm2mpf1  22742  opnnei  23063  neindisj2  23066  cncls2  23216  cncls  23217  cnntr  23218  cnpresti  23231  cnprest  23232  lmcnp  23247  isreg2  23320  ordthauslem  23326  unconn  23372  2ndc1stc  23394  kgen2ss  23498  ptclsg  23558  cnmptcom  23621  kqfvima  23673  hmeof1o  23707  fbncp  23782  fbfinnfr  23784  trfbas2  23786  isufil2  23851  ufprim  23852  trufil  23853  filufint  23863  hausflim  23924  flimrest  23926  flimcls  23928  cnpfcf  23984  alexsubALT  23994  tmdgsum  24038  opnsubg  24051  cldsubg  24054  qustgpopn  24063  tsmsxp  24098  blpnf  24341  blssps  24368  blss  24369  blssec  24379  neibl  24445  prdsxmslem2  24473  xrsmopn  24757  metnrm  24807  climcncf  24849  iccpnfhmeo  24899  xrhmeo  24900  bndth  24913  cphsqrtcl3  25144  iscau2  25234  iscmet3lem2  25249  bcthlem5  25285  bcth3  25288  ishl2  25327  ivthlem1  25409  cmmbl  25492  iundisj2  25507  voliunlem2  25509  mbfaddlem  25618  itg2itg1  25694  itg2seq  25700  itg2mulclem  25704  cnplimc  25845  dvres2  25870  deg1nn0clb  26052  deg1lt0  26053  deg1ge  26060  plypf1  26174  plyadd  26179  plymul  26180  coeeu  26187  dgrub2  26197  coeidlem  26199  coeid3  26202  coemullem  26212  coe11  26215  coemulhi  26216  coemulc  26217  dgreq0  26228  dgrlt  26229  dgradd2  26231  vieta1lem2  26276  tanord1  26503  tanord  26504  logccne0  26544  cxpeq0  26644  cxpmul2z  26657  cxpcn3lem  26714  rtprmirr  26727  relogbzcl  26741  angpieqvd  26798  o1cxp  26942  scvxcvx  26953  chtublem  27179  bposlem3  27254  lgsqr  27319  2sqnn  27407  dchrisumlema  27456  dchrisumlem2  27458  ostth2lem3  27603  nosepon  27634  noextenddif  27637  nolesgn2o  27640  nogesgn1o  27642  nosepne  27649  nodense  27661  onnolt  28224  onslt  28225  onsiso  28226  bdayn0p1  28315  bdayn0sf1o  28316  tghilberti2  28622  inagswap  28825  f1otrg  28855  brbtwn2  28889  axpasch  28925  axcontlem4  28951  axcontlem5  28952  upgredg2vtx  29125  usgredg2vtxeuALT  29206  sizusglecusg  29448  upgredginwlk  29621  frgrwopreg1  30304  frgrwopreg2  30305  frgrregorufrg  30312  lpni  30466  ipasslem5  30821  htthlem  30903  omlsii  31389  spansni  31543  spansneleq  31556  elspansn4  31559  sumspansn  31635  homco1  31787  homulass  31788  mdsl0  32296  ssdmd1  32299  ssdmd2  32300  cvdmd  32323  chirredlem2  32377  atdmd  32384  atmd2  32386  disjif  32564  iundisj2f  32576  isoun  32684  preiman0  32692  padct  32702  iocinioc2  32761  iundisj2fi  32779  sgn3da  32818  sgnnbi  32822  sgnpbi  32823  indpi1  32842  archiabllem1a  33194  archiabllem2a  33197  slmdvsdi  33217  ordtconnlem1  33960  measinblem  34256  measres  34258  measdivcstALTV  34261  mbfmco2  34302  orvclteinc  34513  bnj605  34943  bnj607  34952  bnj964  34979  bnj1033  35005  bnj1128  35026  bnj1137  35031  bnj1136  35033  bnj1413  35071  bnj60  35098  fineqvac  35133  cusgredgex  35149  subgrwlk  35159  acycgr1v  35176  cvmlift2lem10  35339  msubvrs  35587  wsuclem  35848  dfrdg4  35974  brcolinear2  36081  brsegle2  36132  nn0prpw  36346  ntruni  36350  clsint2  36352  fnessref  36380  fnemeet2  36390  fnejoin2  36392  limsucncmpi  36468  ee7.2aOLD  36484  bj-idreseq  37185  dissneqlem  37363  isbasisrelowllem1  37378  isbasisrelowllem2  37379  icoreclin  37380  poimirlem9  37658  poimirlem30  37679  poimirlem32  37681  areacirc  37742  filbcmb  37769  mettrifi  37786  heiborlem8  37847  heiborlem10  37849  heibor  37850  riscer  38017  igenval2  38095  lshpcmp  39011  eqlkr  39122  lkrlsp2  39126  lkrshp  39128  cvrnbtwn2  39298  cvlexch3  39355  cvlexch4N  39356  cvlatexchb1  39357  cvlsupr3  39367  exatleN  39428  cvratlem  39445  atcvrj2b  39456  cvrat3  39466  cvrat4  39467  athgt  39480  ps-1  39501  ps-2  39502  3atlem5  39511  3at  39514  llnneat  39538  llnmlplnN  39563  lplnneat  39569  lplnnelln  39570  islpln2a  39572  lplnriaN  39574  lplnribN  39575  lplnexllnN  39588  2llnjaN  39590  lvolnle3at  39606  lvolneatN  39612  lvolnelln  39613  lvolnelpln  39614  islvol2aN  39616  dalem62  39758  pmapglb2N  39795  pmapglb2xN  39796  lncmp  39807  paddasslem14  39857  paddasslem15  39858  pmod2iN  39873  hlmod1i  39880  pclfinclN  39974  osumcllem8N  39987  pexmidlem4N  39997  pl42lem1N  40003  pl42lem4N  40006  lhpexle1  40032  lhpexle2lem  40033  lhpmcvr5N  40051  lhpmcvr6N  40052  ltrneq  40173  trlnidatb  40201  cdleme0ex2N  40248  cdleme27a  40391  cdleme17d3  40520  cdlemeg46gfre  40556  cdleme48gfv1  40560  cdlemeg49lebilem  40563  cdlemf2  40586  cdlemf  40587  cdlemfnid  40588  trlord  40593  cdlemg31c  40723  cdlemg35  40737  trlcone  40752  tendoeq2  40798  cdlemj3  40847  cdlemk26b-3  40929  cdlemk33N  40933  cdleml3N  41002  cdlemn  41236  dih1dimb2  41265  dihord5apre  41286  dihmeetlem1N  41314  dihglblem5apreN  41315  dihglblem2N  41318  dihglblem3N  41319  dihmeetlem13N  41343  dihmeetlem15N  41345  dihatexv  41362  hdmap14lem12  41903  uzindd  41995  lcmineqlem1  42047  sticksstones1  42164  dvdsexpnn0  42352  frlmfzowrdb  42502  oddcomabszz  42943  jm2.19lem4  42991  fiuneneq  43191  idomsubgmo  43192  omcl2  43332  pwinfi3  43562  gneispa  44129  mnringmulrcld  44227  grumnudlem  44284  ismnushort  44300  binomcxplemnn0  44348  addrcom  44474  int3  44612  suctrALT  44825  suctrALTcf  44921  suctrALT3  44923  chordthmALT  44932  iunconnlem2  44934  relpmin  44952  relpfrlem  44953  stoweidlem26  46035  stoweidlem34  46043  issald  46342  goldbachth  47541  grlimgrtri  47988  nnsgrp  48132  ply1mulgsumlem1  48342  lubsscl  48914  glbsscl  48915