Theorem 3expia 1122

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 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 456	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

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

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 1089

This theorem is referenced by:  ad5ant125  1369  mp3an3  1453  3gencl  3486  vtocl3gaf  3538  vtocl3ga  3540  moi  3678  disji  5085  disjord  5089  3optocl  5729  sossfld  6152  f1oresrab  7082  f1cdmsn  7238  soisores  7283  isomin  7293  isofrlem  7296  ovmpos  7516  ov2gf  7517  ndmovord  7558  nnsuc  7836  poxp  8080  frpoins3xp3g  8093  brtpos  8187  dfsmo2  8289  smoiun  8303  smoord  8307  smogt  8309  omeulem1  8519  omeu  8522  oewordi  8529  uniinqs  8746  mapvalg  8785  pmvalg  8786  elmapg  8788  xpdom3  9015  mapdom3  9089  sdomdomtrfi  9137  domsdomtrfi  9138  php  9143  php3  9145  nndomog  9149  onomeneq  9150  sucdom  9156  unxpdomlem3  9170  isinf  9177  f1finf1o  9185  isfinite2  9210  prfi  9236  ordiso  9433  cnfcom3clem  9626  r111  9699  tskwe  9874  pr2ne  9927  infxpenlem  9935  dfac8alem  9951  infdif  10130  infdif2  10131  cff1  10180  coflim  10183  cfslbn  10189  cfslb2n  10190  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  fin23lem27  10250  isf32lem9  10283  isf34lem6  10302  axcc2lem  10358  domtriomlem  10364  axdc4lem  10377  zorn2lem2  10419  axdclem2  10442  konigthlem  10491  gchen1  10548  gchen2  10549  gchpwdom  10593  gchaleph  10594  winainflem  10616  tskcard  10704  gruiun  10722  gruen  10735  intgru  10737  grudomon  10740  grur1a  10742  grutsk1  10744  nqereu  10852  nqereq  10858  ltsonq  10892  prlem934  10956  reclem3pr  10972  1re  11144  axsup  11220  addlid  11328  recex  11781  lemul1a  12007  lt2msq  12039  fimaxre2  12099  zdiv  12574  zextlt  12578  prime  12585  uzind2  12597  fzind  12602  lbzbi  12861  qbtwnxr  13127  qextltlem  13129  xralrple  13132  xltneg  13144  xlt2add  13187  supxrgtmnf  13256  ixxub  13294  ixxlb  13295  ioo0  13298  ico0  13319  ioc0  13320  icc0  13321  iocssre  13355  icossre  13356  iccssre  13357  fzen  13469  expclzlem  14018  expaddz  14041  expmulz  14043  hashgadd  14312  hashunsngx  14328  hashgt23el  14359  elovmpowrd  14493  pfxnd0  14624  ccatopth2  14652  pfxccatin12  14668  cshf1  14745  shftuz  15004  cau3lem  15290  caubnd  15294  climuni  15487  lo1resb  15499  o1resb  15501  o1of2  15548  o1add  15549  o1mul  15550  o1sub  15551  ntrivcvgmul  15837  eflt  16054  moddvds  16202  dvdscmulr  16223  dvdsmulcr  16224  dvdsle  16249  divalglem8  16339  divalgb  16343  ndvdssub  16348  bitsfzo  16374  gcdcllem1  16438  gcdcllem3  16440  dvdsgcd  16483  nn0rppwr  16500  nn0expgcd  16503  lcmgcdlem  16545  lcmfeq0b  16569  qredeu  16597  isprm3  16622  prmdvdsexpr  16656  prmexpb  16658  eulerthlem2  16721  fermltl  16723  coprimeprodsq  16748  pythagtrip  16774  pcprendvds  16780  pcpremul  16783  pcdvdsb  16809  pc2dvds  16819  4sqlem12  16896  4sqlem18  16902  vdwlem10  16930  cshwshashlem3  17037  xpsrnbas  17504  ismred  17533  mrieqv2d  17574  iscatd  17608  isfuncd  17801  fthestrcsetc  18085  fthsetcestrc  18100  poslubd  18346  dirtr  18537  mulgaddcom  19040  ghmrn  19170  pmtrprfv3  19395  mndodcongi  19484  oddvdsnn0  19485  oddvds  19488  odcl2  19506  odhash3  19517  gexdvds  19525  pgpfi  19546  lsmss1b  19607  lsmss2b  19609  efgsrel  19675  efgred  19689  cntzcmn  19781  cyggenod  19825  lt6abl  19836  gsumcom2  19916  pgpfac1lem2  20018  pgpfac1lem3  20020  dvdsunit  20327  unitmulclb  20329  irredrmul  20375  isabvd  20757  lmodvsdi  20848  lss0cl  20910  islbs3  21122  lbsextlem2  21126  xrsdsreclblem  21379  psrbaglefi  21894  mvrf1  21953  coe1fzgsumd  22260  gsummoncoe1  22264  evl1gsumd  22313  scmataddcl  22472  scmatsubcl  22473  mdetunilem9  22576  mdetuni0  22577  mdetmul  22579  m2cpmrngiso  22714  pm2mpf1  22755  opnnei  23076  neindisj2  23079  cncls2  23229  cncls  23230  cnntr  23231  cnpresti  23244  cnprest  23245  lmcnp  23260  isreg2  23333  ordthauslem  23339  unconn  23385  2ndc1stc  23407  kgen2ss  23511  ptclsg  23571  cnmptcom  23634  kqfvima  23686  hmeof1o  23720  fbncp  23795  fbfinnfr  23797  trfbas2  23799  isufil2  23864  ufprim  23865  trufil  23866  filufint  23876  hausflim  23937  flimrest  23939  flimcls  23941  cnpfcf  23997  alexsubALT  24007  tmdgsum  24051  opnsubg  24064  cldsubg  24067  qustgpopn  24076  tsmsxp  24111  blpnf  24353  blssps  24380  blss  24381  blssec  24391  neibl  24457  prdsxmslem2  24485  xrsmopn  24769  metnrm  24819  climcncf  24861  iccpnfhmeo  24911  xrhmeo  24912  bndth  24925  cphsqrtcl3  25155  iscau2  25245  iscmet3lem2  25260  bcthlem5  25296  bcth3  25299  ishl2  25338  ivthlem1  25420  cmmbl  25503  iundisj2  25518  voliunlem2  25520  mbfaddlem  25629  itg2itg1  25705  itg2seq  25711  itg2mulclem  25715  cnplimc  25856  dvres2  25881  deg1nn0clb  26063  deg1lt0  26064  deg1ge  26071  plypf1  26185  plyadd  26190  plymul  26191  coeeu  26198  dgrub2  26208  coeidlem  26210  coeid3  26213  coemullem  26223  coe11  26226  coemulhi  26227  coemulc  26228  dgreq0  26239  dgrlt  26240  dgradd2  26242  vieta1lem2  26287  tanord1  26514  tanord  26515  logccne0  26555  cxpeq0  26655  cxpmul2z  26668  cxpcn3lem  26725  rtprmirr  26738  relogbzcl  26752  angpieqvd  26809  o1cxp  26953  scvxcvx  26964  chtublem  27190  bposlem3  27265  lgsqr  27330  2sqnn  27418  dchrisumlema  27467  dchrisumlem2  27469  ostth2lem3  27614  nosepon  27645  noextenddif  27648  nolesgn2o  27651  nogesgn1o  27653  nosepne  27660  nodense  27672  onnolt  28274  onlts  28275  oniso  28279  bdayn0p1  28377  bdayn0sf1o  28378  tghilberti2  28722  inagswap  28925  f1otrg  28955  brbtwn2  28990  axpasch  29026  axcontlem4  29052  axcontlem5  29053  upgredg2vtx  29226  usgredg2vtxeuALT  29307  sizusglecusg  29549  upgredginwlk  29721  frgrwopreg1  30405  frgrwopreg2  30406  frgrregorufrg  30413  lpni  30568  ipasslem5  30923  htthlem  31005  omlsii  31491  spansni  31645  spansneleq  31658  elspansn4  31661  sumspansn  31737  homco1  31889  homulass  31890  mdsl0  32398  ssdmd1  32401  ssdmd2  32402  cvdmd  32425  chirredlem2  32479  atdmd  32486  atmd2  32488  disjif  32665  iundisj2f  32677  isoun  32792  preiman0  32800  padct  32808  iocinioc2  32870  iundisj2fi  32888  sgn3da  32926  sgnnbi  32930  sgnpbi  32931  indpi1  32952  archiabllem1a  33285  archiabllem2a  33288  slmdvsdi  33309  ordtconnlem1  34102  measinblem  34398  measres  34400  measdivcstALTV  34403  mbfmco2  34443  orvclteinc  34654  bnj605  35083  bnj607  35092  bnj964  35119  bnj1033  35145  bnj1128  35166  bnj1137  35171  bnj1136  35173  bnj1413  35211  bnj60  35238  rankfilimb  35279  r1filim  35281  fineqvac  35294  fineqvnttrclselem3  35301  fineqvnttrclse  35302  cusgredgex  35338  subgrwlk  35348  acycgr1v  35365  cvmlift2lem10  35528  msubvrs  35776  wsuclem  36039  dfrdg4  36167  brcolinear2  36274  brsegle2  36325  nn0prpw  36539  ntruni  36543  clsint2  36545  fnessref  36573  fnemeet2  36583  fnejoin2  36585  limsucncmpi  36661  ee7.2aOLD  36677  bj-idreseq  37417  dissneqlem  37595  isbasisrelowllem1  37610  isbasisrelowllem2  37611  icoreclin  37612  poimirlem9  37880  poimirlem30  37901  poimirlem32  37903  areacirc  37964  filbcmb  37991  mettrifi  38008  heiborlem8  38069  heiborlem10  38071  heibor  38072  riscer  38239  igenval2  38317  eldisjim3  39066  eldisjs6  39191  lshpcmp  39364  eqlkr  39475  lkrlsp2  39479  lkrshp  39481  cvrnbtwn2  39651  cvlexch3  39708  cvlexch4N  39709  cvlatexchb1  39710  cvlsupr3  39720  exatleN  39780  cvratlem  39797  atcvrj2b  39808  cvrat3  39818  cvrat4  39819  athgt  39832  ps-1  39853  ps-2  39854  3atlem5  39863  3at  39866  llnneat  39890  llnmlplnN  39915  lplnneat  39921  lplnnelln  39922  islpln2a  39924  lplnriaN  39926  lplnribN  39927  lplnexllnN  39940  2llnjaN  39942  lvolnle3at  39958  lvolneatN  39964  lvolnelln  39965  lvolnelpln  39966  islvol2aN  39968  dalem62  40110  pmapglb2N  40147  pmapglb2xN  40148  lncmp  40159  paddasslem14  40209  paddasslem15  40210  pmod2iN  40225  hlmod1i  40232  pclfinclN  40326  osumcllem8N  40339  pexmidlem4N  40349  pl42lem1N  40355  pl42lem4N  40358  lhpexle1  40384  lhpexle2lem  40385  lhpmcvr5N  40403  lhpmcvr6N  40404  ltrneq  40525  trlnidatb  40553  cdleme0ex2N  40600  cdleme27a  40743  cdleme17d3  40872  cdlemeg46gfre  40908  cdleme48gfv1  40912  cdlemeg49lebilem  40915  cdlemf2  40938  cdlemf  40939  cdlemfnid  40940  trlord  40945  cdlemg31c  41075  cdlemg35  41089  trlcone  41104  tendoeq2  41150  cdlemj3  41199  cdlemk26b-3  41281  cdlemk33N  41285  cdleml3N  41354  cdlemn  41588  dih1dimb2  41617  dihord5apre  41638  dihmeetlem1N  41666  dihglblem5apreN  41667  dihglblem2N  41670  dihglblem3N  41671  dihmeetlem13N  41695  dihmeetlem15N  41697  dihatexv  41714  hdmap14lem12  42255  uzindd  42347  lcmineqlem1  42399  sticksstones1  42516  dvdsexpnn0  42704  frlmfzowrdb  42874  oddcomabszz  43301  jm2.19lem4  43349  fiuneneq  43549  idomsubgmo  43550  omcl2  43690  pwinfi3  43919  gneispa  44486  mnringmulrcld  44584  grumnudlem  44641  ismnushort  44657  binomcxplemnn0  44705  addrcom  44830  int3  44968  suctrALT  45181  suctrALTcf  45277  suctrALT3  45279  chordthmALT  45288  iunconnlem2  45290  relpmin  45308  relpfrlem  45309  stoweidlem26  46384  stoweidlem34  46392  issald  46691  goldbachth  47907  grlimgrtri  48363  nnsgrp  48537  ply1mulgsumlem1  48746  lubsscl  49319  glbsscl  49320