Theorem 3expia 1120

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ad5ant125  1365  mp3an3  1449  3gencl  3474  moi  3654  disji  5058  disjord  5063  3optocl  5684  sossfld  6094  f1oresrab  7008  f1cdmsn  7163  soisores  7207  isomin  7217  isofrlem  7220  ovmpos  7430  ov2gf  7431  ndmovord  7471  nnsuc  7739  poxp  7978  brtpos  8060  dfsmo2  8187  smoiun  8201  smoord  8205  smogt  8207  omeulem1  8422  omeu  8425  oewordi  8431  uniinqs  8595  mapvalg  8634  pmvalg  8635  elmapg  8637  xpdom3  8866  mapdom3  8945  sdomdomtrfi  8996  domsdomtrfi  8997  php  9002  php3  9004  nndomog  9008  php3OLD  9016  onomeneq  9020  sucdom  9027  unxpdomlem3  9038  isinf  9045  findcard2OLD  9065  isfinite2  9081  ordiso  9284  cnfcom3clem  9472  r111  9542  tskwe  9717  pr2ne  9770  infxpenlem  9778  dfac8alem  9794  infdif  9974  infdif2  9975  cff1  10023  coflim  10026  cfslbn  10032  cfslb2n  10033  cofsmo  10034  cfsmolem  10035  cfcoflem  10037  fin23lem27  10093  isf32lem9  10126  isf34lem6  10145  axcc2lem  10201  domtriomlem  10207  axdc4lem  10220  zorn2lem2  10262  axdclem2  10285  konigthlem  10333  gchen1  10390  gchen2  10391  gchpwdom  10435  gchaleph  10436  winainflem  10458  tskcard  10546  gruiun  10564  gruen  10577  intgru  10579  grudomon  10582  grur1a  10584  grutsk1  10586  nqereu  10694  nqereq  10700  ltsonq  10734  prlem934  10798  reclem3pr  10814  1re  10984  axsup  11059  addid2  11167  recex  11616  lemul1a  11838  lt2msq  11869  fimaxre2  11929  zdiv  12399  zextlt  12403  prime  12410  uzind2  12422  fzind  12427  lbzbi  12685  qbtwnxr  12943  qextltlem  12945  xralrple  12948  xltneg  12960  xlt2add  13003  supxrgtmnf  13072  ixxub  13109  ixxlb  13110  ioo0  13113  ico0  13134  ioc0  13135  icc0  13136  iocssre  13168  icossre  13169  iccssre  13170  fzen  13282  expclzlem  13815  expaddz  13836  expmulz  13838  hashgadd  14101  hashunsngx  14117  hashgt23el  14148  elovmpowrd  14270  pfxnd0  14410  ccatopth2  14439  pfxccatin12  14455  cshf1  14532  shftuz  14789  cau3lem  15075  caubnd  15079  climuni  15270  lo1resb  15282  o1resb  15284  o1of2  15331  o1add  15332  o1mul  15333  o1sub  15334  ntrivcvgmul  15623  eflt  15835  moddvds  15983  dvdscmulr  16003  dvdsmulcr  16004  dvdsle  16028  divalglem8  16118  divalgb  16122  ndvdssub  16127  bitsfzo  16151  gcdcllem1  16215  gcdcllem3  16217  dvdsgcd  16261  lcmgcdlem  16320  lcmfeq0b  16344  qredeu  16372  isprm3  16397  prmdvdsexpr  16431  prmexpb  16434  eulerthlem2  16492  fermltl  16494  coprimeprodsq  16518  pythagtrip  16544  pcprendvds  16550  pcpremul  16553  pcdvdsb  16579  pc2dvds  16589  4sqlem12  16666  4sqlem18  16672  vdwlem10  16700  cshwshashlem3  16808  xpsrnbas  17291  ismred  17320  mrieqv2d  17357  iscatd  17391  isfuncd  17589  fthestrcsetc  17876  fthsetcestrc  17891  poslubd  18140  dirtr  18329  mulgaddcom  18736  ghmrn  18856  pmtrprfv3  19071  mndodcongi  19160  oddvdsnn0  19161  oddvds  19164  odcl2  19181  odhash3  19190  gexdvds  19198  pgpfi  19219  lsmss1b  19281  lsmss2b  19283  efgsrel  19349  efgred  19363  cntzcmn  19450  cyggenod  19493  lt6abl  19505  gsumcom2  19585  pgpfac1lem2  19687  pgpfac1lem3  19689  dvdsunit  19914  unitmulclb  19916  irredrmul  19958  isabvd  20089  lmodvsdi  20155  lss0cl  20217  islbs3  20426  lbsextlem2  20430  xrsdsreclblem  20653  psrbaglefi  21144  mvrf1  21203  coe1fzgsumd  21482  gsummoncoe1  21484  evl1gsumd  21532  scmataddcl  21674  scmatsubcl  21675  mdetunilem9  21778  mdetuni0  21779  mdetmul  21781  m2cpmrngiso  21916  pm2mpf1  21957  opnnei  22280  neindisj2  22283  cncls2  22433  cncls  22434  cnntr  22435  cnpresti  22448  cnprest  22449  lmcnp  22464  isreg2  22537  ordthauslem  22543  unconn  22589  2ndc1stc  22611  kgen2ss  22715  ptclsg  22775  cnmptcom  22838  kqfvima  22890  hmeof1o  22924  fbncp  22999  fbfinnfr  23001  trfbas2  23003  isufil2  23068  ufprim  23069  trufil  23070  filufint  23080  hausflim  23141  flimrest  23143  flimcls  23145  cnpfcf  23201  alexsubALT  23211  tmdgsum  23255  opnsubg  23268  cldsubg  23271  qustgpopn  23280  tsmsxp  23315  blpnf  23559  blssps  23586  blss  23587  blssec  23597  neibl  23666  prdsxmslem2  23694  xrsmopn  23984  metnrm  24034  climcncf  24072  iccpnfhmeo  24117  xrhmeo  24118  bndth  24130  cphsqrtcl3  24360  iscau2  24450  iscmet3lem2  24465  bcthlem5  24501  bcth3  24504  ishl2  24543  ivthlem1  24624  cmmbl  24707  iundisj2  24722  voliunlem2  24724  mbfaddlem  24833  itg2itg1  24910  itg2seq  24916  itg2mulclem  24920  cnplimc  25060  dvres2  25085  deg1nn0clb  25264  deg1lt0  25265  deg1ge  25272  plypf1  25382  plyadd  25387  plymul  25388  coeeu  25395  dgrub2  25405  coeidlem  25407  coeid3  25410  coemullem  25420  coe11  25423  coemulhi  25424  coemulc  25425  dgreq0  25435  dgrlt  25436  dgradd2  25438  vieta1lem2  25480  tanord1  25702  tanord  25703  logccne0  25743  cxpeq0  25842  cxpmul2z  25855  cxpcn3lem  25909  relogbzcl  25933  angpieqvd  25990  o1cxp  26133  scvxcvx  26144  chtublem  26368  bposlem3  26443  lgsqr  26508  2sqnn  26596  dchrisumlema  26645  dchrisumlem2  26647  ostth2lem3  26792  tghilberti2  27008  inagswap  27211  f1otrg  27241  brbtwn2  27282  axpasch  27318  axcontlem4  27344  axcontlem5  27345  upgredg2vtx  27520  usgredg2vtxeuALT  27598  sizusglecusg  27839  upgredginwlk  28012  frgrwopreg1  28691  frgrwopreg2  28692  frgrregorufrg  28699  lpni  28851  ipasslem5  29206  htthlem  29288  omlsii  29774  spansni  29928  spansneleq  29941  elspansn4  29944  sumspansn  30020  homco1  30172  homulass  30173  mdsl0  30681  ssdmd1  30684  ssdmd2  30685  cvdmd  30708  chirredlem2  30762  atdmd  30769  atmd2  30771  disjif  30926  iundisj2f  30938  isoun  31043  preiman0  31051  padct  31063  iocinioc2  31109  iundisj2fi  31127  archiabllem1a  31454  archiabllem2a  31457  slmdvsdi  31477  ordtconnlem1  31883  indpi1  31997  measinblem  32197  measres  32199  measdivcstALTV  32202  mbfmco2  32241  orvclteinc  32451  sgn3da  32517  sgnnbi  32521  sgnpbi  32522  bnj605  32896  bnj607  32905  bnj964  32932  bnj1033  32958  bnj1128  32979  bnj1137  32984  bnj1136  32986  bnj1413  33024  bnj60  33051  fineqvac  33075  cusgredgex  33092  subgrwlk  33103  acycgr1v  33120  cvmlift2lem10  33283  msubvrs  33531  frpoins3xp3g  33797  wsuclem  33828  nosepon  33877  noextenddif  33880  nolesgn2o  33883  nogesgn1o  33885  nosepne  33892  nodense  33904  dfrdg4  34262  brcolinear2  34369  brsegle2  34420  nn0prpw  34521  ntruni  34525  clsint2  34527  fnessref  34555  fnemeet2  34565  fnejoin2  34567  limsucncmpi  34643  ee7.2aOLD  34659  bj-idreseq  35342  dissneqlem  35520  isbasisrelowllem1  35535  isbasisrelowllem2  35536  icoreclin  35537  poimirlem9  35795  poimirlem30  35816  poimirlem32  35818  areacirc  35879  filbcmb  35907  mettrifi  35924  heiborlem8  35985  heiborlem10  35987  heibor  35988  riscer  36155  igenval2  36233  lshpcmp  37009  eqlkr  37120  lkrlsp2  37124  lkrshp  37126  cvrnbtwn2  37296  cvlexch3  37353  cvlexch4N  37354  cvlatexchb1  37355  cvlsupr3  37365  exatleN  37425  cvratlem  37442  atcvrj2b  37453  cvrat3  37463  cvrat4  37464  athgt  37477  ps-1  37498  ps-2  37499  3atlem5  37508  3at  37511  llnneat  37535  llnmlplnN  37560  lplnneat  37566  lplnnelln  37567  islpln2a  37569  lplnriaN  37571  lplnribN  37572  lplnexllnN  37585  2llnjaN  37587  lvolnle3at  37603  lvolneatN  37609  lvolnelln  37610  lvolnelpln  37611  islvol2aN  37613  dalem62  37755  pmapglb2N  37792  pmapglb2xN  37793  lncmp  37804  paddasslem14  37854  paddasslem15  37855  pmod2iN  37870  hlmod1i  37877  pclfinclN  37971  osumcllem8N  37984  pexmidlem4N  37994  pl42lem1N  38000  pl42lem4N  38003  lhpexle1  38029  lhpexle2lem  38030  lhpmcvr5N  38048  lhpmcvr6N  38049  ltrneq  38170  trlnidatb  38198  cdleme0ex2N  38245  cdleme27a  38388  cdleme17d3  38517  cdlemeg46gfre  38553  cdleme48gfv1  38557  cdlemeg49lebilem  38560  cdlemf2  38583  cdlemf  38584  cdlemfnid  38585  trlord  38590  cdlemg31c  38720  cdlemg35  38734  trlcone  38749  tendoeq2  38795  cdlemj3  38844  cdlemk26b-3  38926  cdlemk33N  38930  cdleml3N  38999  cdlemn  39233  dih1dimb2  39262  dihord5apre  39283  dihmeetlem1N  39311  dihglblem5apreN  39312  dihglblem2N  39315  dihglblem3N  39316  dihmeetlem13N  39340  dihmeetlem15N  39342  dihatexv  39359  hdmap14lem12  39900  uzindd  39992  lcmineqlem1  40044  sticksstones1  40109  metakunt1  40132  metakunt5  40136  frlmfzowrdb  40242  nn0rppwr  40340  nn0expgcd  40342  dvdsexpnn0  40348  rtprmirr  40354  oddcomabszz  40773  jm2.19lem4  40821  fiuneneq  41029  idomsubgmo  41030  pwinfi3  41177  gneispa  41747  mnringmulrcld  41853  grumnudlem  41910  ismnushort  41926  binomcxplemnn0  41974  addrcom  42100  int3  42239  suctrALT  42453  suctrALTcf  42549  suctrALT3  42551  chordthmALT  42560  iunconnlem2  42562  stoweidlem26  43574  stoweidlem34  43582  issald  43879  goldbachth  45010  nnsgrp  45382  ply1mulgsumlem1  45738  lubsscl  46265  glbsscl  46266