Theorem 3expia 1139

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ad5ant125OLD  1391  mp3an3  1479  3gencl  3498  vtocl3gaf  3544  vtocl3ga  3545  moi  3681  disji  5094  disjord  5098  3optocl  5758  sossfld  6184  f1oresrab  7123  f1cdmsn  7280  soisores  7325  isomin  7335  isofrlem  7338  ovmpos  7558  ov2gf  7559  ndmovord  7600  nnsuc  7876  poxp  8120  frpoins3xp3g  8133  brtpos  8227  dfsmo2  8330  smoiun  8344  smoord  8348  smogt  8350  omeulem1  8563  omeu  8566  oewordi  8573  uniinqs  8791  mapvalg  8829  pmvalg  8830  elmapg  8832  xpdom3  9059  mapdom3  9133  sdomdomtrfi  9181  domsdomtrfi  9182  php  9187  php3  9189  nndomog  9193  onomeneq  9194  sucdom  9200  unxpdomlem3  9214  isinf  9221  f1finf1o  9229  isfinite2  9254  prfi  9279  ordiso  9474  cnfcom3clem  9670  r111  9743  tskwe  9932  pr2ne  9985  infxpenlem  9993  dfac8alem  10009  infdif  10187  infdif2  10188  cff1  10237  coflim  10240  cfslbn  10246  cfslb2n  10247  cofsmo  10248  cfsmolem  10249  cfcoflem  10251  fin23lem27  10307  isf32lem9  10340  isf34lem6  10359  axcc2lem  10415  domtriomlem  10421  axdc4lem  10434  zorn2lem2  10476  axdclem2  10499  konigthlem  10548  gchen1  10605  gchen2  10606  gchpwdom  10650  gchaleph  10651  winainflem  10673  tskcard  10761  gruiun  10779  gruen  10792  intgru  10794  grudomon  10797  grur1a  10799  grutsk1  10801  nqereu  10909  nqereq  10915  ltsonq  10949  prlem934  11013  reclem3pr  11029  1re  11203  axsup  11280  addlid  11388  recex  11841  lemul1a  12064  lt2msq  12095  fimaxre2  12155  indpi1  12227  zdiv  12661  zextlt  12665  prime  12672  uzind2  12684  fzind  12689  lbzbi  12955  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  13564  expclzlem  14115  expaddz  14138  expmulz  14140  hashgadd  14409  hashunsngx  14425  hashgt23el  14457  elovmpowrd  14591  pfxnd0  14722  ccatopth2  14750  pfxccatin12  14766  cshf1  14843  shftuz  15102  sgn3da  15134  sgnnbi  15137  sgnpbi  15138  cau3lem  15402  caubnd  15406  climuni  15599  lo1resb  15611  o1resb  15613  o1of2  15660  o1add  15661  o1mul  15662  o1sub  15663  ntrivcvgmul  15952  eflt  16168  moddvds  16316  dvdscmulr  16337  dvdsmulcr  16338  dvdsle  16363  divalglem8  16453  divalgb  16457  ndvdssub  16462  bitsfzo  16488  gcdcllem1  16552  gcdcllem3  16554  dvdsgcd  16597  nn0rppwr  16614  nn0expgcd  16617  lcmgcdlem  16659  lcmfeq0b  16683  qredeu  16711  isprm3  16736  prmdvdsexpr  16771  prmexpb  16773  eulerthlem2  16836  fermltl  16838  coprimeprodsq  16863  pythagtrip  16889  pcprendvds  16895  pcpremul  16898  pcdvdsb  16924  pc2dvds  16934  4sqlem12  17011  4sqlem18  17017  vdwlem10  17045  cshwshashlem3  17152  xpsrnbas  17620  ismred  17649  mrieqv2d  17690  iscatd  17724  isfuncd  17917  fthestrcsetc  18201  fthsetcestrc  18216  poslubd  18462  dirtr  18653  mulgaddcom  19159  ghmrn  19294  pmtrprfv3  19519  mndodcongi  19608  oddvdsnn0  19609  oddvds  19612  odcl2  19630  odhash3  19641  gexdvds  19649  pgpfi  19670  lsmss1b  19731  lsmss2b  19733  efgsrel  19799  efgred  19813  cntzcmn  19905  cyggenod  19949  lt6abl  19960  gsumcom2  20040  pgpfac1lem2  20142  pgpfac1lem3  20144  dvdsunit  20457  unitmulclb  20459  irredrmul  20505  isabvd  20915  lmodvsdi  21006  lss0cl  21068  islbs3  21279  lbsextlem2  21283  rspprop  21370  xrsdsreclblem  21563  psrbaglefi  22076  mvrf1  22135  coe1fzgsumd  22464  gsummoncoe1  22468  evl1gsumd  22517  scmataddcl  22673  scmatsubcl  22674  mdetunilem9  22777  mdetuni0  22778  mdetmul  22780  m2cpmrngiso  22915  pm2mpf1  22956  opnnei  23277  neindisj2  23280  cncls2  23430  cncls  23431  cnntr  23432  cnpresti  23445  cnprest  23446  lmcnp  23461  isreg2  23534  ordthauslem  23540  unconn  23586  2ndc1stc  23608  kgen2ss  23712  ptclsg  23772  cnmptcom  23835  kqfvima  23887  hmeof1o  23921  fbncp  23996  fbfinnfr  23998  trfbas2  24000  isufil2  24065  ufprim  24066  trufil  24067  filufint  24077  hausflim  24138  flimrest  24140  flimcls  24142  cnpfcf  24198  alexsubALT  24208  tmdgsum  24252  opnsubg  24265  cldsubg  24268  qustgpopn  24277  tsmsxp  24312  blpnf  24554  blssps  24581  blss  24582  blssec  24592  neibl  24658  prdsxmslem2  24686  xrsmopn  24970  metnrm  25020  climcncf  25059  iccpnfhmeo  25104  xrhmeo  25105  bndth  25117  cphsqrtcl3  25346  iscau2  25436  iscmet3lem2  25451  bcthlem5  25487  bcth3  25490  ishl2  25529  ivthlem1  25610  cmmbl  25693  iundisj2  25708  voliunlem2  25710  mbfaddlem  25819  itg2itg1  25895  itg2seq  25901  itg2mulclem  25905  cnplimc  26046  dvres2  26071  deg1nn0clb  26247  deg1lt0  26248  deg1ge  26255  plypf1  26369  plyadd  26374  plymul  26375  coeeu  26382  dgrub2  26392  coeidlem  26394  coeid3  26397  coemullem  26407  coe11  26410  coemulhi  26411  coemulc  26412  dgreq0  26422  dgrlt  26423  dgradd2  26425  vieta1lem2  26472  tanord1  26702  tanord  26703  logccne0  26743  cxpeq0  26843  cxpmul2z  26856  cxpcn3lem  26912  rtprmirr  26925  relogbzcl  26939  angpieqvd  26996  o1cxp  27139  scvxcvx  27150  chtublem  27375  bposlem3  27450  lgsqr  27515  2sqnn  27603  dchrisumlema  27652  dchrisumlem2  27654  ostth2lem3  27799  nosepon  27829  noextenddif  27832  nolesgn2o  27835  nogesgn1o  27837  nosepne  27844  nodense  27856  onnolt  28459  onlts  28460  oniso  28464  bdayn0p1  28562  bdayn0sf1o  28563  tghilberti2  28911  inagswap  29158  f1otrg  29220  brbtwn2  29255  axpasch  29291  axcontlem4  29317  axcontlem5  29318  upgredg2vtx  29491  usgredg2vtxeuALT  29572  sizusglecusg  29813  upgredginwlk  29985  frgrwopreg1  30669  frgrwopreg2  30670  frgrregorufrg  30677  lpni  30832  ipasslem5  31187  htthlem  31269  omlsii  31755  spansni  31909  spansneleq  31922  elspansn4  31925  sumspansn  32001  homco1  32153  homulass  32154  mdsl0  32662  ssdmd1  32665  ssdmd2  32666  cvdmd  32689  chirredlem2  32743  atdmd  32750  atmd2  32752  disjif  32923  iundisj2f  32935  isoun  33047  preiman0  33055  padct  33063  iocinioc2  33124  iundisj2fi  33142  archiabllem1a  33511  archiabllem2a  33514  slmdvsdi  33535  ordtconnlem1  34314  measinblem  34610  measres  34612  measdivcstALTV  34615  mbfmco2  34655  orvclteinc  34866  bnj605  35295  bnj607  35304  bnj964  35331  bnj1033  35357  bnj1128  35378  bnj1137  35383  bnj1136  35385  bnj1413  35423  bnj60  35450  rankfilimb  35496  r1filim  35498  nelscottrankgt  35518  fineqvac  35529  fineqvnttrclselem3  35536  fineqvnttrclse  35537  vonf1oonfo  35599  cusgredgex  35614  subgrwlk  35624  acycgr1v  35641  cvmlift2lem10  35804  msubvrs  36052  wsuclem  36315  dfrdg4  36443  brcolinear2  36550  brsegle2  36601  nn0prpw  36834  ntruni  36838  clsint2  36840  fnessref  36868  fnemeet2  36878  fnejoin2  36880  limsucncmpi  36956  ee7.2aOLD  36972  bj-idreseq  37806  dissneqlem  37986  isbasisrelowllem1  38001  isbasisrelowllem2  38002  icoreclin  38003  poimirlem9  38280  poimirlem30  38301  poimirlem32  38303  areacirc  38364  filbcmb  38391  mettrifi  38408  heiborlem8  38469  heiborlem10  38471  heibor  38472  riscer  38639  igenval2  38717  eldisjim3  39464  eldisjs6  39589  lshpcmp  39762  eqlkr  39873  lkrlsp2  39877  lkrshp  39879  cvrnbtwn2  40049  cvlexch3  40106  cvlexch4N  40107  cvlatexchb1  40108  cvlsupr3  40118  exatleN  40178  cvratlem  40195  atcvrj2b  40206  cvrat3  40216  cvrat4  40217  athgt  40230  ps-1  40251  ps-2  40252  3atlem5  40261  3at  40264  llnneat  40288  llnmlplnN  40313  lplnneat  40319  lplnnelln  40320  islpln2a  40322  lplnriaN  40324  lplnribN  40325  lplnexllnN  40338  2llnjaN  40340  lvolnle3at  40356  lvolneatN  40362  lvolnelln  40363  lvolnelpln  40364  islvol2aN  40366  dalem62  40508  pmapglb2N  40545  pmapglb2xN  40546  lncmp  40557  paddasslem14  40607  paddasslem15  40608  pmod2iN  40623  hlmod1i  40630  pclfinclN  40724  osumcllem8N  40737  pexmidlem4N  40747  pl42lem1N  40753  pl42lem4N  40756  lhpexle1  40782  lhpexle2lem  40783  lhpmcvr5N  40801  lhpmcvr6N  40802  ltrneq  40923  trlnidatb  40951  cdleme0ex2N  40998  cdleme27a  41141  cdleme17d3  41270  cdlemeg46gfre  41306  cdleme48gfv1  41310  cdlemeg49lebilem  41313  cdlemf2  41336  cdlemf  41337  cdlemfnid  41338  trlord  41343  cdlemg31c  41473  cdlemg35  41487  trlcone  41502  tendoeq2  41548  cdlemj3  41597  cdlemk26b-3  41679  cdlemk33N  41683  cdleml3N  41752  cdlemn  41986  dih1dimb2  42015  dihord5apre  42036  dihmeetlem1N  42064  dihglblem5apreN  42065  dihglblem2N  42068  dihglblem3N  42069  dihmeetlem13N  42093  dihmeetlem15N  42095  dihatexv  42112  hdmap14lem12  42653  uzindd  42745  lcmineqlem1  42796  sticksstones1  42913  dvdsexpnn0  43095  frlmfzowrdb  43278  oddcomabszz  43671  jm2.19lem4  43719  fiuneneq  43919  idomsubgmo  43920  omcl2  44060  pwinfi3  44289  gneispa  44856  mnringmulrcld  44952  grumnudlem  44995  ismnushort  45011  binomcxplemnn0  45059  addrcom  45183  int3  45321  suctrALT  45534  suctrALTcf  45630  suctrALT3  45632  chordthmALT  45641  iunconnlem2  45643  relpmin  45661  relpfrlem  45662  stoweidlem26  46740  stoweidlem34  46748  issald  47047  goldbachth  48299  nprmdvdsfacm1  48376  grlimgrtri  48768  nnsgrp  48942  ply1mulgsumlem1  49166  lubsscl  49738  glbsscl  49739